Nuprl Lemma : safety_and
4,23
postcript
pdf
A
:Type,
P
,
Q
:((
A
List)
Prop).
safety(
A
;
x
.
P
(
x
))
safety(
A
;
x
.
Q
(
x
))
safety(
A
;
x
.
P
(
x
) &
Q
(
x
))
latex
Definitions
safety(
A
;
tr
.
P
(
tr
))
,
{
T
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
Prop
,
x
(
s
)
,
l1
l2
,
P
&
Q
Lemmas
iseg
wf
origin
A:Type, P, Q:((A List)
Prop).
safety(A;x.Q(x)) safety(A;x.P(x) & Q(x)) A:Type, P, Q:((A List)Prop).
safety(A;x.Q(x)) safety(A;x.P(x) & Q(x)) Qx:A. B(x)
T
l2